$\forall$$T$:Type, ${\it eq}$:EqDecider($T$), ${\it as}$,${\it bs}$:($T$ List).
\\[0ex]($\forall$$x$:$T$. ($x$ $\in$ list{-}diff(${\it eq}$; ${\it as}$; ${\it bs}$)) $\Leftarrow\!\Rightarrow$ (($x$ $\in$ ${\it as}$) $\wedge$ ($\neg$($x$ $\in$ ${\it bs}$))))
\\[0ex]$\wedge$ (no\_repeats($T$; ${\it as}$) $\Rightarrow$ no\_repeats($T$; list{-}diff(${\it eq}$; ${\it as}$; ${\it bs}$)))